Formal verification has been widely used in providing a formal proof of electronic designs to prove the correctness of electronic designs. Modern electronic designs have grown exponentially in both their sizes and complexities and have thus rendered formal verification increasingly harder. Counters have been widely used in digital portions of electronic designs. A counter is an electronic device that often functions in conjunction with clock signals and stores the number of times a particular event has occurred. Counters affect the performance of formal engines by, for example, increasing the sequential depth for formal engines. For example, the number of iterations in the reachability analysis of formal verification may be proportional to the number of possible counts in the counters. Counters may not necessarily be assigned some arbitrary values because specific values for counters as well as relationships among counters may be of some particular significance to an electronic design, and arbitrarily assigned values may nevertheless lead to undesirable or unreliable verification results.
Therefore, there exists a need for a method, system, and computer program product for enhancing formal verification with counter acceleration for electronic designs.